(set-logic QF_LRA)
(declare-fun v0 () Bool)
(declare-fun v1 () Bool)
(declare-fun v2 () Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v6 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun v9 () Bool)
(declare-fun r0 () Real)
(declare-fun r4 () Real)
(declare-fun r7 () Real)
(declare-fun r8 () Real)
(declare-fun r9 () Real)
(declare-fun r10 () Real)
(declare-fun r11 () Real)
(declare-fun r14 () Real)
(declare-fun r15 () Real)
(declare-fun v10 () Bool)
(assert v0)
(declare-fun v11 () Bool)
(declare-fun r17 () Real)
(declare-fun r18 () Real)
(declare-fun v13 () Bool)
(assert (< 0.175 r0))
(push 3)
(push 4)
(declare-fun r21 () Real)
(assert (not (< 0.175 r0)))
(declare-fun v21 () Bool)
(assert (=> (not (< 0.175 r0)) (< 0.175 r0)))
(assert (= (+ 3157.0 r15) (- r10)))
(push 4)
(declare-fun v22 () Bool)
(push 2)
(assert v11)
(assert (=> v21 (< r15 (+ (+ r18 0.994) r17))))
(push 1)
(pop 12)
(check-sat)
